minus2(x, x) -> 0
minus2(x, y) -> cond3(min2(x, y), x, y)
cond3(y, x, y) -> s1(minus2(x, s1(y)))
min2(0, v) -> 0
min2(u, 0) -> 0
min2(s1(u), s1(v)) -> s1(min2(u, v))
min2(s1(x0), s1(x1))
cond3(x0, x1, x0)
minus2(x0, x1)
min2(x0, 0)
min2(0, x0)
↳ QTRS
↳ DependencyPairsProof
minus2(x, x) -> 0
minus2(x, y) -> cond3(min2(x, y), x, y)
cond3(y, x, y) -> s1(minus2(x, s1(y)))
min2(0, v) -> 0
min2(u, 0) -> 0
min2(s1(u), s1(v)) -> s1(min2(u, v))
min2(s1(x0), s1(x1))
cond3(x0, x1, x0)
minus2(x0, x1)
min2(x0, 0)
min2(0, x0)
MIN2(s1(u), s1(v)) -> MIN2(u, v)
COND3(y, x, y) -> MINUS2(x, s1(y))
MINUS2(x, y) -> MIN2(x, y)
MINUS2(x, y) -> COND3(min2(x, y), x, y)
minus2(x, x) -> 0
minus2(x, y) -> cond3(min2(x, y), x, y)
cond3(y, x, y) -> s1(minus2(x, s1(y)))
min2(0, v) -> 0
min2(u, 0) -> 0
min2(s1(u), s1(v)) -> s1(min2(u, v))
min2(s1(x0), s1(x1))
cond3(x0, x1, x0)
minus2(x0, x1)
min2(x0, 0)
min2(0, x0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
MIN2(s1(u), s1(v)) -> MIN2(u, v)
COND3(y, x, y) -> MINUS2(x, s1(y))
MINUS2(x, y) -> MIN2(x, y)
MINUS2(x, y) -> COND3(min2(x, y), x, y)
minus2(x, x) -> 0
minus2(x, y) -> cond3(min2(x, y), x, y)
cond3(y, x, y) -> s1(minus2(x, s1(y)))
min2(0, v) -> 0
min2(u, 0) -> 0
min2(s1(u), s1(v)) -> s1(min2(u, v))
min2(s1(x0), s1(x1))
cond3(x0, x1, x0)
minus2(x0, x1)
min2(x0, 0)
min2(0, x0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
MIN2(s1(u), s1(v)) -> MIN2(u, v)
minus2(x, x) -> 0
minus2(x, y) -> cond3(min2(x, y), x, y)
cond3(y, x, y) -> s1(minus2(x, s1(y)))
min2(0, v) -> 0
min2(u, 0) -> 0
min2(s1(u), s1(v)) -> s1(min2(u, v))
min2(s1(x0), s1(x1))
cond3(x0, x1, x0)
minus2(x0, x1)
min2(x0, 0)
min2(0, x0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
MIN2(s1(u), s1(v)) -> MIN2(u, v)
min2(s1(x0), s1(x1))
cond3(x0, x1, x0)
minus2(x0, x1)
min2(x0, 0)
min2(0, x0)
min2(s1(x0), s1(x1))
cond3(x0, x1, x0)
minus2(x0, x1)
min2(x0, 0)
min2(0, x0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
MIN2(s1(u), s1(v)) -> MIN2(u, v)
From the DPs we obtained the following set of size-change graphs:
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ UsableRulesProof
COND3(y, x, y) -> MINUS2(x, s1(y))
MINUS2(x, y) -> COND3(min2(x, y), x, y)
minus2(x, x) -> 0
minus2(x, y) -> cond3(min2(x, y), x, y)
cond3(y, x, y) -> s1(minus2(x, s1(y)))
min2(0, v) -> 0
min2(u, 0) -> 0
min2(s1(u), s1(v)) -> s1(min2(u, v))
min2(s1(x0), s1(x1))
cond3(x0, x1, x0)
minus2(x0, x1)
min2(x0, 0)
min2(0, x0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ UsableRulesProof
COND3(y, x, y) -> MINUS2(x, s1(y))
MINUS2(x, y) -> COND3(min2(x, y), x, y)
min2(0, v) -> 0
min2(u, 0) -> 0
min2(s1(u), s1(v)) -> s1(min2(u, v))
min2(s1(x0), s1(x1))
cond3(x0, x1, x0)
minus2(x0, x1)
min2(x0, 0)
min2(0, x0)
cond3(x0, x1, x0)
minus2(x0, x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ UsableRulesProof
COND3(y, x, y) -> MINUS2(x, s1(y))
MINUS2(x, y) -> COND3(min2(x, y), x, y)
min2(0, v) -> 0
min2(u, 0) -> 0
min2(s1(u), s1(v)) -> s1(min2(u, v))
min2(s1(x0), s1(x1))
min2(x0, 0)
min2(0, x0)
MINUS2(x0, 0) -> COND3(0, x0, 0)
MINUS2(0, x0) -> COND3(0, 0, x0)
MINUS2(s1(x0), s1(x1)) -> COND3(s1(min2(x0, x1)), s1(x0), s1(x1))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ UsableRulesProof
MINUS2(s1(x0), s1(x1)) -> COND3(s1(min2(x0, x1)), s1(x0), s1(x1))
COND3(y, x, y) -> MINUS2(x, s1(y))
MINUS2(0, x0) -> COND3(0, 0, x0)
MINUS2(x0, 0) -> COND3(0, x0, 0)
min2(0, v) -> 0
min2(u, 0) -> 0
min2(s1(u), s1(v)) -> s1(min2(u, v))
min2(s1(x0), s1(x1))
min2(x0, 0)
min2(0, x0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ UsableRulesProof
MINUS2(s1(x0), s1(x1)) -> COND3(s1(min2(x0, x1)), s1(x0), s1(x1))
COND3(y, x, y) -> MINUS2(x, s1(y))
MINUS2(0, x0) -> COND3(0, 0, x0)
min2(0, v) -> 0
min2(u, 0) -> 0
min2(s1(u), s1(v)) -> s1(min2(u, v))
min2(s1(x0), s1(x1))
min2(x0, 0)
min2(0, x0)
MINUS2(0, s1(z0)) -> COND3(0, 0, s1(z0))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ UsableRulesProof
MINUS2(0, s1(z0)) -> COND3(0, 0, s1(z0))
COND3(y, x, y) -> MINUS2(x, s1(y))
MINUS2(s1(x0), s1(x1)) -> COND3(s1(min2(x0, x1)), s1(x0), s1(x1))
min2(0, v) -> 0
min2(u, 0) -> 0
min2(s1(u), s1(v)) -> s1(min2(u, v))
min2(s1(x0), s1(x1))
min2(x0, 0)
min2(0, x0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ UsableRulesProof
COND3(y, x, y) -> MINUS2(x, s1(y))
MINUS2(s1(x0), s1(x1)) -> COND3(s1(min2(x0, x1)), s1(x0), s1(x1))
min2(0, v) -> 0
min2(u, 0) -> 0
min2(s1(u), s1(v)) -> s1(min2(u, v))
min2(s1(x0), s1(x1))
min2(x0, 0)
min2(0, x0)
COND3(s1(y_0), s1(z0), s1(y_0)) -> MINUS2(s1(z0), s1(s1(y_0)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ UsableRulesProof
MINUS2(s1(x0), s1(x1)) -> COND3(s1(min2(x0, x1)), s1(x0), s1(x1))
COND3(s1(y_0), s1(z0), s1(y_0)) -> MINUS2(s1(z0), s1(s1(y_0)))
min2(0, v) -> 0
min2(u, 0) -> 0
min2(s1(u), s1(v)) -> s1(min2(u, v))
min2(s1(x0), s1(x1))
min2(x0, 0)
min2(0, x0)
MINUS2(s1(z1), s1(s1(z0))) -> COND3(s1(min2(z1, s1(z0))), s1(z1), s1(s1(z0)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ UsableRulesProof
MINUS2(s1(z1), s1(s1(z0))) -> COND3(s1(min2(z1, s1(z0))), s1(z1), s1(s1(z0)))
COND3(s1(y_0), s1(z0), s1(y_0)) -> MINUS2(s1(z0), s1(s1(y_0)))
min2(0, v) -> 0
min2(u, 0) -> 0
min2(s1(u), s1(v)) -> s1(min2(u, v))
min2(s1(x0), s1(x1))
min2(x0, 0)
min2(0, x0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
COND3(y, x, y) -> MINUS2(x, s1(y))
MINUS2(x, y) -> COND3(min2(x, y), x, y)
min2(0, v) -> 0
min2(u, 0) -> 0
min2(s1(u), s1(v)) -> s1(min2(u, v))
min2(s1(x0), s1(x1))
cond3(x0, x1, x0)
minus2(x0, x1)
min2(x0, 0)
min2(0, x0)
cond3(x0, x1, x0)
minus2(x0, x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
COND3(y, x, y) -> MINUS2(x, s1(y))
MINUS2(x, y) -> COND3(min2(x, y), x, y)
min2(0, v) -> 0
min2(u, 0) -> 0
min2(s1(u), s1(v)) -> s1(min2(u, v))
min2(s1(x0), s1(x1))
min2(x0, 0)
min2(0, x0)